\newcommand{\MM}{\emph{MM}\xspace}
\newcommand{\R}{R\xspace}
\newcommand{\lR}{\overleftarrow{\R}\xspace}
\newcommand{\rR}{\overrightarrow{\R}\xspace}


%For the remainder of this paper, we will restrict ourselves to transformations between two metamodels for simplicity purposes, although most concepts could be generalized to multi-directional transformations.

\section{Generating the solution space as a model with uncertainty}\label{sec:jtl-gen-un}

There are many reasons why managing a set of models explicitly is impractical. Thus, in this section we propose a new semantics for the JTL engine able to automatically generate models with uncertainty. In order to establish what are the basic requirements the semantic extension must satisfy, we provide a rigorous characterization of the non-deterministic transformations based on that given in~\cite{S09} first, then we extend it to the case with uncertainty.

\subsection{Non-determinism and uncertainty in bidirectional transformations}
Non-deterministic bidirectional transformations as defined in~\cite{CDEP10} must be characterized also according to the multiplicity of the solution space. By following the notation used in~\cite{S09} we can give a characterization for this category of bidirectional transformations. In particular, a bidirectional transformation can be considered as a relation $\R\subseteq M\times N$ which can be given in terms of the following directional mappings 
\begin{eqnarray}
    \label{eq:right}   \rR: M\times N\rightarrow N^*\\
    \label{eq:left}    \lR: M\times N\rightarrow M^*
\end{eqnarray}
where $M^*$ and $N^*$ are the Kleene closures of the metamodels $M$ and $N$, respectively\footnote{Although different methods can be given for defining a set of models, in this paper we assume that a metamodel corresponds to a set of models.}. The main difference with the work in~\cite{S09} is represented by the fact that the mappings yield an arbitrary number of models accounting for the transformation non-determinism. Although we only described the support for bidirectional transformations, the approach can easily be generalized to the multi-directional scenario, where updates on multiple models are propagated to a designated target. Generally, transformations can be executed in two modes: 
\begin{itemize}
\item[--] \emph{checkonly} mode, where the models are simply checked for consistency, denoted as $\R(m,n)$ with $m\in M, n\in N$; and
\item[--] \emph{enforce} mode, where $\rR$ or $\lR$ is applied to inconsistent models in order to restore consistency, depending on which of the two models should be updated.
\end{itemize}
% 
When the transformations propagate an update the result is expected to be consistent. Formally, we say that the transformation $\rR$ is {correct} whenever applied to inconsistent models $(m,n)$ enforces the relation $\R$ as follows $\lR(m,n'_i) = m$ for any $n'_i$ in the solution space $\rR(m,n) = \langle n'_1 \cdots n'_k \rangle\in N^*$. We assumed that $n$ is the model whose consistency has to be restored. Similarly, $\lR$ can propagate changes in the opposite direction\footnote{Please note that in contrasts with the set theory the notion of injectivity in models is local, i.e., the $\overrightarrow{R}$ and $\overleftarrow{R}$ mappings can be both injective or non-injective on disjoint sets of model elements belonging to the same model, which justifies the target multiplicity on both mappings.}.

%\paragraph{Hyppocraticness.} 
Another important property a transformation must satisfy is the {hyppocraticness} also known as {check-then-enforce} principle: if two models are already consistent then both $\rR$ and $\lR$ must leave the models unchanged. More formally
\begin{eqnarray}
    \label{eq:hypp-right}\R(m,n) & \implies & \rR(m, n) = n\\
    \label{eq:hypp-left}\R(m,n) & \implies & \lR(m,n) = m 
\end{eqnarray}
The conditions above are the same of the unary case~\cite{S09} since non-determinism occurs only when the consistency has to be restored, therefore these conditions are valid also for non-deterministic transformations.

\medskip
\noindent
Within the new implementation of the JTL transformation engine, we distinguish two different behaviors
\begin{itemize}
\item[--] \emph{extensive}, the directional mappings $\rR$ and $\lR$ generate a complete solution space consisting of all the models satisfying the relation as described above;
\item[--] \emph{intensive} (or with \emph{uncertainty}), the directional mappings $\rR_u$ and $\lR_u$ generate a model with uncertainty which is semantically equivalent to the models of the extensive case.
\end{itemize}
%
However, one important issue arising from this scenario is that models with uncertainty may be over-approximations of the sets of transformation candidates. This is due to the "combinatorial" nature of these models since each point of uncertainty collects the different alternatives. Consequently, it can happen that certain combinations produce concretizations which are not part of the extensive solution space. Therefore, besides the models with uncertainty it is important to generate also those constraints which limit the solution to the admissible concretization only.

In particular, the model with uncertainty conforms to the metamodel construction given in Sect.~\ref{sec:metamodel}, then the directional mappings for the intensive case are defined as follows
\begin{eqnarray}
    \rR_u: M\times N\rightarrow U(N)\times\emph{OCL}\\
    \lR_u: M\times N\rightarrow U(M)\times\emph{OCL}
\end{eqnarray}
with $U(N)$ and $U(M)$ the uncertainty extensions of the $N$ and $M$ metamodels, respectively. Thus, if $(m,n)\not\in\R$ are two non-consistent models, the transformation $\rR_u(m,n)$ generates a model with uncertainty $\bar{n}$ and a predicate $p_N$ then the transformation is said correct if enforces the relation $R$ as follows
$$\emph{concr}(\lR_u(m,n')) = m = \lR(m,n')$$ 
for any $n'\in\emph{refine}(p_N,\bar{n})$ with $\lR_u(m,n')$ denoting for simplicity the model with uncertainty outcome of the transformation. 

In the next section, we illustrate how the transformation engine has been extended and more specifically how the models with uncertainty and the related refinement predicates are generated by means of traceability information which are dynamically produced by the engine itself.

\subsection{Generating models with uncertainty}\label{sec:jtl-gen-un} 
In order to generate the model with uncertainty the JTL engine needs to cross-link the corresponding model elements throughout the solution space. This is obtained by {logically} connecting those elements in the source model which originated the same target element. Within JTL, the ASP-based engine can derive how models are related by means of a deductive process. To this end, the existing traceability management offers enough expressiveness to understand how the models can be factorized by identifying those elements which are connected among them.

In particular, tracing information stores the relationships between source and target model elements at execution-time;  by means of them, for each source model element, the applied transformation rules and the correspondent generated target elements are given. 
In essence, tracing information represents the linkage between models established by a transformation execution. To better understand how JTL works, let us consider the following definitions.

\begin{definition}[domain] If $m\in M$ and $n\in M$ are two consistent models $R(m,n)$, then the tracing domain $U$ consists of a triple $(|m|,|n|,|R|)$ with $|m|$, $|n|$, and $|R|$ the set of models elements of $m$ and $n$ and transformation rules in $R$, respectively. 
\end{definition}
Each different transformation application gives place to a different tracing domain. Elements within a domain represents the linkage which denotes how a target element \emph{can} been generated starting from a source one.

\begin{definition}[trace link]
A trace link $u$ consists of a triple $(s,t,r)\in U$ such that \emph{i)} the model element $t$ is obtained from $s$ by the rule $r$, and \emph{ii)} $id(t)=id(s)$, with $id$ denoting the identity of any model element. 
\end{definition}
For the sake of brevity, whenever it does not cause confusion the identity of the model elements in a trace link $u$ is denoted by $id(u)$. A tracing $\Phi$ is the set of all trace links $u\in U$, with $U$ domain of $R(m,n)$.

\begin{definition}[connection]
Let $\phi$ be a subset of $\Phi$, then $\phi$ is called logical connection if for any $u, v\in\phi$ the corresponding identities are the same, i.e., $id(u) = id(v)$.
\end{definition}
The logical connection is of crucial relevance because from each connection a point of uncertainty is generated. In the following, we describe how the engine utilizes the connections for generating the u


An excerpt of the implemented mechanism in given in Listing \ref{lst:newJTLengine}. In particular, lines 1-6 contains a portion of the ASP encoding for the transition \emph{print} of the state machine model and the generated four alternative transitions \emph{print} of the hierarchical state machine model given in Fig.~\ref{fig:HSM2SMmodels2}; whereas in lines 8-11 the corresponding trace links are given. 
During the execution of the transformation, the engine is able to deduce both the concretization models and/or the model with uncertainty. Any point of uncertainty is deduced by calculating the logic connection among model elements (lines 15-21).

\begin{lstlisting}[breaklines,style=AMMA,language=ASPencoding,mathescape,rulesepcolor=\color{black},caption={ A fragment of the adapted JTL engine},captionpos=b, aboveskip=0.2cm, belowskip=0.1cm, label={lst:newJTLengine}]
node(SM, p, transition).

node(HSM, p1, transition).
node(HSM, p2, transition).
node(HSM, p3, transition).
node(HSM, p4, transition).

trace_link(tl1,s1,t1,r1).
trace_link(tl2,s1,t2,r2).
trace_link(tl1,s1,t3,r3).
trace_link(tl2,s1,t4,r4).

getID(p,s1). getID(p1,t1). getID(p2,t2). getID(p3,t3). getID(p4,t4). 

is_logically_connected(t1,t2) :- trace_link(tl1,s1,t1), trace_link(tl2,s2,t2),
                                 equals_id(s1,s2), equals_id(t1,t2).
node(UMM,ID,UMC) :-  is_logically_connected(t1,t2), getID(ID,t1), 
                     getUMM(UMM,t1), getUMC(UMC,t1). 
edge(UMM,IDe,URef,ID,IDt) :- is_logically_connected(t1,t2), getID(ID,t1), 
                             getUMM(UMM,t1), getRefID(IDe,ID), 
                             getChildID(IDt,ID), getURef(URef,t1). 
                               
\end{lstlisting}
%\vspace{-0.2cm} 



\noindent
Considering the generated solutions in the right-hand side of Fig.~\ref{fig:HSM2SMmodels2}, the corresponding model with uncertainty is in Fig.~\ref{fig:UMHSM}. In particular, the alternative transitions are collected in a point of uncertainty (\code{UTransition}) which contains the transitions targeting each one of the nested states within \code{Active} as well as to the composite state itself. 

As already mentioned in Sect.~\ref{sec:jtl-gen-un}, models with uncertainty may over-approximate the sets of transformation candidates. For instance, the scenario in Fig.~\ref{fig:stateMachines} suggests that only one \code{print} transition can exist in the final model. However, the generated model with uncertainty admits also models with multiple \code{print} transitions giving place to more concretizations than those expected. Therefore, in order to avoid multiple \code{print} transitions, the model with uncertainty in Fig.~\ref{fig:UHSM} is augmented with a constraint that reduces the concretizations to cases with one \code{print} transition only. According to the uncertainty metamodel described in Sect.~\ref{sec:metamodel}, each metaclass provide an attribute \code{ref} to maintain the reference to the corresponding concretization(s). E.g., the model fragment in Listing~\ref{lst:xmi} shows that each transition refers to a different concretization by means of the \code{ref} tag. Then, the following OCL constraint is automatically derived 
%
\begin{lstlisting}[breaklines,style=AMMA,language=ASPencoding,mathescape,rulesepcolor=\color{black}, numbers=none]    
Transition.allInstances()->collect(e | e.transitions)->select(e:Transition | 
e.ref = "HSMm_1.xmi#/" xor e.ref = "HSMm_2.xmi#/"  xor e.ref = "HSMm_3.xmi#/"  
xor e.ref = "HSMm_4.xmi#/")
\end{lstlisting}
%
and applied by means of the \emph{refine} operators. A technical point arises when the derived predicate is not cross-linking different points of uncertainty and, consequently, does not deal with all the combination of variants. In such cases, the predicate is a transform which returns another model with uncertainty which exactly denotes the intended concretizations. 
 



